\section{Передача продолжений}

$\Lambda$ --- мета-оператор, ``\llang{;;}'' --- мета-операция:

$$
S\llang{;;}\Lambda = S
$$

$$
S_1\llang{;;}S_2 = S_1\llang{;}S_2
$$

$$
\withenv{\Lambda}{\trans{c}{\llang{skip}}{c}}\ruleno{SkipEmpty$_{cps}$}
$$

$$
\withenv{\Lambda}{\trans{\inbr{s,i,o}}{\mbox{$x\llang{:=}e$}}{\inbr{s[x\gets\sembr{e}\;s],i,o}}}\ruleno{AssignEmpty$_{cps}$}
$$

$$
\withenv{\Lambda}{\trans{\inbr{s,zi,o}}{\mbox{$\llang{read}\;x$}}{\inbr{s[x\gets z],i,o}}}\ruleno{ReadEmpty$_{cps}$}
$$

$$
\withenv{\Lambda}{\trans{\inbr{s,i,o}}{\mbox{$\llang{write}\;e$}}{\inbr{s,i,o(\sembr{e}\;s)}}}\ruleno{WriteEmpty$_{cps}$}
$$

$$
\trule{\withenv{\Lambda}{\trans{c}{\inmath{K}}{c^\prime}}}
      {\withenv{K}{\trans{c}{\llang{skip}}{c^\prime}}}\ruleno{Skip$_{cps}$}
$$

$$
\trule{\withenv{\Lambda}{\trans{\inbr{s[x\gets\sembr{e}\;s],i,o}}{\inmath{K}}{c^\prime}}}
      {\withenv{K}{\trans{\inbr{s,i,o}}{\mbox{$x\llang{:=}e$}}{c^\prime}}}\ruleno{Assign$_{cps}$}
$$

$$
\trule{\withenv{\Lambda}{\trans{\inbr{s[x\gets z],i,o}}{\inmath{K}}{c^\prime}}}
      {\withenv{K}{\trans{\inbr{s,zi,o}}{\mbox{$\llang{read}\;x$}}{c^\prime}}}\ruleno{Read$_{cps}$}
$$

$$
\trule{\withenv{\Lambda}{\trans{\inbr{s,i,o(\sembr{e}\;s)}}{\inmath{K}}{c^\prime}}}
      {\withenv{K}{\trans{\inbr{s,i,o}}{\mbox{$\llang{write}\;e$}}{c^\prime}}}\ruleno{Write$_{cps}$}
$$

$$
\trule{\withenv{\llang{$S_2\;$;;$\;K$}}{\trans{c}{\inmath{S_1}}{c^\prime}}}
      {\withenv{K}{\trans{c}{\llang{$S_1\;$;$\;S_2$}}{c^\prime}}}\ruleno{Seq$_{cps}$}
$$

$$
\crule{\withenv{K}{\trans{c}{\inmath{S_1}}{c^\prime}}} 
      {\withenv{K}{\trans{c}{\llang{if$\;e\;$then$\;S_1\;$else$\;S_2$}}{c^\prime}}}
      {\sembr{e}\;c.s\ne 0}\ruleno{If-True$_{cps}$}
$$

$$
\crule{\withenv{K}{\trans{c}{\inmath{S_2}}{c^\prime}}} 
      {\withenv{K}{\trans{c}{\llang{if$\;e\;$then$\;S_1\;$else$\;S_2$}}{c^\prime}}}
      {\sembr{e}\;c.s= 0}\ruleno{If-False$_{cps}$}
$$

$$
\crule{\withenv{\llang{while$\;e\;$do$\;S\;$;;$\;K$}}{\trans{c}{\inmath{S}}{c^\prime}}}
      {\withenv{K}{\trans{c}{\llang{while$\;e\;$do$\;S$}}{c^\prime}}}
      {\sembr{e}\;c.s\ne 0}\ruleno{While-True$_{cps}$}
$$

$$
\crule{\withenv{\Lambda}{\trans{c}{\inmath{K}}{c^\prime}}}
      {\withenv{K}{\trans{c}{\llang{while$\;e\;$do$\;S$}}{c^\prime}}}
      {\sembr{e}\;c.s= 0}\ruleno{While-False$_{cps}$}
$$


